package extensionTools.smvCreator;

import java.util.ArrayList;
import java.util.Dictionary;
import java.util.Enumeration;
import java.util.Hashtable;

import extensionTools.smvCreator.Exceptions.RulesUtilsException;
import extensionTools.smvCreator.Exceptions.SmvDBException;
import extensionTools.smvCreator.Link.LinkType;
import extensionTools.smvCreator.Link.SmvType;
import extensionTools.smvCreator.RulesUtils.Assoc;

/**
 * @author Oshrit & Lital
 * This class implements rules for Assoc relation betwen processes and objects, 
 * and between objects and objects.
 */

public class Associations extends Rule 
{                   
     
	Dictionary<String, String[]> assocInstrumentDict;
    Dictionary<String, String[]> assocConditionDict;
    Dictionary<String, String> assocDict;
	/*
      * C'tor
      */
     public Associations(DiagramDatabase db) 
     {
        super(db);
        assocDict = new  Hashtable<String, String>(); 
        assocInstrumentDict = new  Hashtable<String, String[]>(); 
        assocConditionDict =new Hashtable<String, String[]>();
     }

     
     /**
      * 
      *@throws RulesUtilsException - when null parameters were sent to SmvOp
     * @see extensionTools.smvCreator.Rule#createRule()
      */
     @Override
     public String createRule() throws RulesUtilsException 
     {

         String rules = "";
             
         for (SmvProcess currProc : db.getSmvProcessList()) 
         { 
            //create list of all assoc_proc_obj variables only for processes that are father to leafs
             if(currProc.getFatherToLeafs()==true)
             {
            	 //init assoc proc-obj list and obj-obj list
            	 RulesUtils.creatAssocsList(db, currProc);
            	 
                 //create the main rule string of cases related to assoc_obj_obj
                 rules += createRuleForAssocObjects(currProc);
                 
                 ArrayList<SmvObject> objects = db.getSmvObjectList();
         		
                 //create the main rule string of cases related to create assoc_proc_obj
         		for (SmvObject obj : objects) 
         		{    				
     				rules += "\n" + createRuleForAssocProcObject(obj ,currProc, db);
         		}
             } 
         }
         return rules;
     }
        
	/**
	 * This function creating the rule for assoc_proc_obj
	 * @param obj
	 * @param db
	 * @return rule for assoc_proc_obj
	 * @throws RulesUtilsException - when null parameters were sent to SmvOp
	 */
		private String createRuleForAssocProcObject(SmvObject obj, SmvProcess fatherProcess, DiagramDatabase db) throws RulesUtilsException
	 	{
     		String returnRule = "";
     		
     		String objName = obj.getName();
     		String processFatherName="";
     		String assoc = "";
     		String assocNameResultAndMod = "";
     		
     		for (int i=0; i<SMVCreator.K; i++)
     		{    		
     			for (int j=0; j<SMVCreator.K; j++)
     			{
     				//The use of the flag is to prevent duplicate lines
     				//-1 means don't print case at all
     				// 1 means a case is already printed
     				// 0 means a case should be print 
     				int flag = -1;
     				
	     			String[] returnCaseLines = null;
	     			String[] destroyCaseLine = null;
	     			String[] buildingAssoc 	 = null;
	     			String[] destroingAssoc  = null;
	     			
	     			//all the links that get out/to the object obj
	     			ArrayList<Link > objLinks = obj.getLinkList();   
	     			
	     			for (Link lnk : objLinks) 
	     			{
	     				// DEBUG long dstId = lnk.getDstId();

	     				if (lnk.getLinkType() == LinkType.RESULT || 
	     						lnk.getLinkType() == LinkType.EFFECT)
	     				{
	     					flag=0;
	     					
	     					SmvType srcType = lnk.getSrcType();
	     					
	     					//we are looking for only two options, a link between process and object state, 
	     					//or between process and object
	     					if((lnk.getLinkType() != LinkType.EFFECT &&srcType != SmvType.PROCESS)) 
	     						return returnRule;
     				
	     					SmvProcess proc = null;
	     					if (srcType == SmvType.PROCESS)
	     					{
	     						proc = RulesUtils.getProccessbyId(lnk.getSrcId(), db);
	     					}
	     					else
	     					{
	     						proc = RulesUtils.getProccessbyId(lnk.getDstId(), db);
	     					}
	     					
	     					//current process is not a leaf so no association is needed
	     					if (proc.getChildrenIdList().size() != 0)
	     					{
	     						return returnRule;
	     					}
     					
	     					//get the father process
	     					if(proc.getFatherId() == -1)
	     					{
	     						return returnRule;
	     					}
	     					
	     					//change proc to father proc
	     					proc = RulesUtils.getProccessbyId(proc.getFatherId(), db);
	     					   
	     					ArrayList<SmvProcess> childrenList = db.getChildrenList(proc);
	     					
     					
	     					processFatherName = proc.getName();
	     					String processName = db.getProcessNameById(lnk.getDstId());
     					
	     					ArrayList<Link> currXorList= null;
	     					ArrayList<Link> currOrList= null;
	     					
	     					if (lnk.getLinkType() !=  LinkType.EFFECT)
	     					{
	     						processName = db.getProcessNameById(lnk.getSrcId());
	     						currXorList= RulesUtils.lnkInXor(db,lnk);
		     					currOrList= RulesUtils.lnkInOr(db,lnk);
	     					}
	     					if ( currXorList != null)
	     					{
	     						String[] strArray = toArray(CreateAssocXorObject(objName, 
	     								processName,currXorList,true, i,j,SMVCreator.K,processFatherName));
	     						
	     						returnCaseLines=RulesUtils.combineStrings(returnCaseLines, strArray);

	     					}
	     					else if (currOrList != null)
	     					{
	     						String[] strArray = toArray(CreateAssocXorObject(objName, 
     									processName,currOrList,false, i,j,SMVCreator.K,processFatherName));
	     						
     							returnCaseLines=RulesUtils.combineStrings(returnCaseLines, strArray);
     						}
     						else
     						{
     							String initialState = "";
     							State state = obj.getInitialState();
     							if (state != null)
     							{
     								initialState = state.getName();
     							}
	     		
	     						returnCaseLines=RulesUtils.combineStrings(returnCaseLines,
	     											 CreateAssocProcToObj(obj, processName,processFatherName,
	     													initialState,lnk, i, j,  SMVCreator.K));		
     						}
	     					
	     					String[] destroyResult = DestroyAssocProcToObj(obj, proc, childrenList, i,j,SMVCreator.K);
	     					
	     					if(destroyResult[2] == "" || destroyResult[2] == null) //there is no consumption rule
	     					{ 
	     						String[] resultWithoutConsumption = new String[2];
	     						resultWithoutConsumption[0] = destroyResult[0];
	     						resultWithoutConsumption[1] = destroyResult[1];
	     						destroyCaseLine=RulesUtils.combineStrings(destroyCaseLine,resultWithoutConsumption);		
	     					}
	     					else //there is consumption rule
	     					{
	     						destroyCaseLine=RulesUtils.combineStrings(destroyCaseLine,destroyResult);
	     					}

	     						     					
	     					assoc = "assoc_"+processFatherName+"_"+i+"_"+objName+"_"+j;
		         			
		         				         			
	     				}
     				
	     				else if  (lnk.getLinkType() == LinkType.CONSUMPTION && lnk.getLabel() == (""))
	     				{
	     					flag=0;
	     					
	     					SmvProcess proc = RulesUtils.getProccessbyId(lnk.getDstId(), db);
	     					
	     					//current process is not a leaf so no association is needed
	     					if (proc.getChildrenIdList().size() != 0)
	     					{
	     						return returnRule;
	     					}
 					
	     					//get the father process
	     					if(proc.getFatherId() == -1)
	     					{
	     						return returnRule;
	     					}
	     					
	     					//change proc to father proc
	     					proc = RulesUtils.getProccessbyId(proc.getFatherId(), db);
	     					   
	     					ArrayList<SmvProcess> childrenList = db.getChildrenList(proc);
	     					
	     					processFatherName = proc.getName();
	     				    					
	     					String processName = db.getProcessNameById(lnk.getDstId()); 					
	     					
	     					returnCaseLines=RulesUtils.combineStrings(returnCaseLines,
	     							CreateAssocObjToProc(objName, processName,i,j,SMVCreator.K));		
			
							String[] destroyResult = DestroyAssocProcToObj(obj, proc, childrenList, i,j,SMVCreator.K);
							
							if(destroyResult[2] == "" || destroyResult[2] == null) //there is no consumption rule
							{ 
								String[] resultWithoutConsumption = new String[2];
								resultWithoutConsumption[0] = destroyResult[0];
								resultWithoutConsumption[1] = destroyResult[1];
								destroyCaseLine=RulesUtils.combineStrings(destroyCaseLine,resultWithoutConsumption);		
							}
							else //there is consumption rule
							{
								destroyCaseLine=RulesUtils.combineStrings(destroyCaseLine,destroyResult);
							}
					
								     					
							assoc = "assoc_"+objName+"_"+i+"_"+processFatherName+"_"+j;
				
	     				}
	     				else if (lnk.getLinkType() == LinkType.INSTRUMENT )
	     				{
	     					flag = 0;

	     					SmvProcess proc = RulesUtils.getProccessbyId(lnk.getDstId(), db);
	     					
	     					//current process is not a leaf so no association is needed
	     					if (proc.getChildrenIdList().size() != 0)
	     					{
	     						return returnRule;
	     					}
 					
	     					//get the father process
	     					if(proc.getFatherId() == -1)
	     					{
	     						return returnRule;
	     					}
	     					
	     					//change proc to father proc
	     					proc = RulesUtils.getProccessbyId(proc.getFatherId(), db);
	     					processFatherName = proc.getName();
	     					String processName = db.getProcessNameById(lnk.getDstId());
	     					
	     					returnCaseLines = RulesUtils.combineStrings(returnCaseLines,
	     							CreateAssocObjToProc(objName, processName,i,j,SMVCreator.K));	
	     					
	     					assoc = "assocInstrument_"+objName+"_"+i+"_"+processFatherName+"_"+j;
	     						
	     					
	     				}
	     				else if (lnk.getLinkType() == LinkType.CONDITION)
	     				{
	     					flag = 0;

	     					SmvProcess proc = RulesUtils.getProccessbyId(lnk.getDstId(), db);
	     					
	     					//current process is not a leaf so no association is needed
	     					if (proc.getChildrenIdList().size() != 0)
	     					{
	     						return returnRule;
	     					}
 					
	     					//get the father process
	     					if(proc.getFatherId() == -1)
	     					{
	     						return returnRule;
	     					}
	     					
	     					//change proc to father proc
	     					proc = RulesUtils.getProccessbyId(proc.getFatherId(), db);
	     					processFatherName = proc.getName();
	     					String processName = db.getProcessNameById(lnk.getDstId());
	     					
	     					returnCaseLines = RulesUtils.combineStrings(returnCaseLines,
	     							CreateAssocObjToProc(objName, processName,i,j,SMVCreator.K));
	     					
	     					
	     					assoc = "assocCondition_"+objName+"_"+i+"_"+processFatherName+"_"+j;
	     				}

		     			if(flag == 0 )
		     			{
		     				flag =1;
		     				
		     				if(lnk.getLinkType() == LinkType.INSTRUMENT)
		     				{
		     					if(assocInstrumentDict.get(assoc) == null)
		     					{
		     						String[] caseExist = new String[1];
			     		     		caseExist[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ", "ev_terminate"+"_"+processFatherName + "_" + j + " = 0"), "FALSE");
			     					destroyCaseLine = RulesUtils.combineStrings(destroyCaseLine, caseExist);
			     					
		     						assocInstrumentDict.put(assoc, (RulesUtils.combineStrings(returnCaseLines,
			         					destroyCaseLine)));
		     					}
		     					else
		     					{
		     						String[] value = assocInstrumentDict.get(assoc);
		     						String valueString = RulesUtils.stringArrayToString(value);
		     						String returnCaseLinesString = RulesUtils.stringArrayToString(returnCaseLines);
		     						String destroyCaseLineString = RulesUtils.stringArrayToString(destroyCaseLine);
		     						
		     						if(!(returnCaseLinesString.contains(valueString))&&!(destroyCaseLineString.contains(valueString)))
		     						{
		     							assocInstrumentDict.remove(assoc);
		     							assocInstrumentDict.put(assoc, RulesUtils.combineStrings(RulesUtils.combineStrings(value, returnCaseLines),
				         					destroyCaseLine));
		     						}
		     						
		     					}
		     				}
		     				else if(lnk.getLinkType() == LinkType.CONDITION)
		     				{
		     					if(assocConditionDict.get(assoc) == null)
		     					{
		     						String[] caseExist = new String[1];
			     		     		caseExist[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ", "ev_terminate"+"_"+processFatherName +  "_" + j + " = 0"), "FALSE");
			     					destroyCaseLine = RulesUtils.combineStrings(destroyCaseLine, caseExist);
		     						assocConditionDict.put(assoc, (RulesUtils.combineStrings(returnCaseLines,
				         					destroyCaseLine)));
		     					}
		     					else
		     					{
		     						String[] value = assocConditionDict.get(assoc);
	
	     							assocConditionDict.remove(assoc);
		     						assocConditionDict.put(assoc, RulesUtils.combineStrings(RulesUtils.combineStrings(value, returnCaseLines),
			         					destroyCaseLine));
		     						
		     					}
		     				}
		     				else
		     				{		
			         			if (lnk.getLinkType() != LinkType.RESULT && 
			     						lnk.getLinkType() != LinkType.EFFECT)
					         	{
			         				returnCaseLines = RulesUtils.combineStrings(returnCaseLines,
			         					destroyCaseLine);
			         			
			         				returnCaseLines=RulesUtils.addDefaultState(returnCaseLines,"TRUE",
			         					assoc);
			         				
			         				//preventing duplicates
			         				if(assoc != null && assoc != "" && assocDict.get(assoc) == null)
			         				{
			         					assocDict.put(assoc, "");
			         					
			         					returnRule += SmvOp.next
			         					(assoc,SmvOp.createCase(returnCaseLines));
			         				}
			         				
			         				
			         			}
			         			else
			         			{
			         				if (lnk.getLinkType() == LinkType.RESULT || 
			     						 lnk.getLinkType() == LinkType.EFFECT)
			         				{
			     							buildingAssoc=RulesUtils.combineStrings(buildingAssoc,
			     									returnCaseLines);
			     							destroingAssoc = destroyCaseLine;
			     							assocNameResultAndMod = assoc;
			     							String[] temp = RulesUtils.combineStrings(buildingAssoc,
			     									destroyCaseLine);
			     							String[] truecase = {"TRUE: "+ assoc+ ";"};
			     							temp = RulesUtils.combineStrings(temp,truecase); 
			     							if(assocNameResultAndMod != null && assocNameResultAndMod != "" && assocDict.get(assocNameResultAndMod) == null)
			     			     			{
			     			     				assocDict.put(assocNameResultAndMod, "");
			     				     			returnRule += SmvOp.next
			     								(assocNameResultAndMod,SmvOp.createCase(temp));
			     			     			}
			         				
		     						}
			         			}
			         			//clear returnCaseLines for the next link
			         			returnCaseLines = null;
			         		} 

		     			}
	     			}
	     			buildingAssoc = RulesUtils.combineStrings(buildingAssoc,destroingAssoc);
	     			buildingAssoc = RulesUtils.addDefaultState(buildingAssoc, "TRUE", assocNameResultAndMod);
	     			
	     			if(assocNameResultAndMod != null && assocNameResultAndMod != "" && assocDict.get(assocNameResultAndMod) == null)
	     			{
	     				assocDict.put(assocNameResultAndMod, "");
		     			returnRule += SmvOp.next
						(assocNameResultAndMod,SmvOp.createCase(buildingAssoc));
	     			}
     			}
     		}
     		
     		String[] returnCaseLines = null;
     		Enumeration<?> keys = assocInstrumentDict.keys();
     		int i=0;
     		while (keys!=null && i<assocInstrumentDict.size()) 
     		{ 			
     			String key = (String)keys.nextElement();
     			String[] value = assocInstrumentDict.get(key);

     			returnCaseLines=RulesUtils.addDefaultState(value,"TRUE", key);
     			//preventing duplicates
     			if(key != null && key != "" && assocDict.get(key) == null)
     			{
	     			assocDict.put(key, "");
     				returnRule += SmvOp.next(key,SmvOp.createCase(returnCaseLines));
     			}
     				i++;
     			
			}
     		
     		returnCaseLines = null;
     		keys = assocConditionDict.keys();
     		i=0;
     		while (keys!=null && i<assocConditionDict.size()) 
     		{ 			
     			String key = (String)keys.nextElement();
     			String[] value = assocConditionDict.get(key);

     			returnCaseLines=RulesUtils.addDefaultState(value,"TRUE", key);
     			//preventing duplicates
     			if(key != null && key != "" && assocDict.get(key) == null)
     			{
     				assocDict.put(key, "");	
	     			returnRule += SmvOp.next(key,SmvOp.createCase(returnCaseLines));
     			}
     			i++;
     		}

     	return returnRule;
     }
        
		
        
		/**
		 * This function create the rule for the creation of assoc_proc_obj
		 * @param objName
		 * @param processName
		 * @param currPlace
		 * @param currPlaceObj
		 * @param k
		 * @return
		 * @throws RulesUtilsException - when null parameters were sent to SmvOp
		 */
		private String[] CreateAssocObjToProc(String objName, String processName,int currPlace,int currPlaceObj, int k) throws RulesUtilsException 
		{
     		String currObjName = objName + "_"+currPlaceObj;
     		
     		String nextValue = "TRUE";

     		String[] caseExist = new String[1];
     		caseExist[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
     					"ev_activate"+"_"+processName+"_"+currPlace+" = TRUE",
     					"!("+currObjName+"=notExist)"),nextValue);

     		return caseExist;
     	}
		
		/**
		 * This function create the rule for the creation of assoc_proc_obj
		 * @param object
		 * @param initialState 
		 * @param process
		 * @param currPlace
		 * @param currPlaceObj
		 * @param k
		 * @return
		 * @throws RulesUtilsException - when null parameters were sent to SmvOp
		 */
		private String[] CreateAssocProcToObj(SmvObject object, String processName, 
				String processFatherName,String initialState, Link link, int currPlace,int currPlaceObj, int k)
				throws RulesUtilsException 
		{

     		String nextValue = "TRUE";
     		String objName = object.getName();
     		String[] caseExist = new String[1];
     		caseExist[0] = "";
     		String otherAsoocs ="";
     		for (int i =0 ;i < SMVCreator.K;i++)
     		{
     			if (i != currPlaceObj && null != processFatherName && processFatherName != "")
     			{
     				otherAsoocs = SmvOp.and(otherAsoocs, "assoc"+"_"+processFatherName+
     									"_"+currPlace+"_"+objName+"_"+i+"=FALSE");
     			}
     		}
     		ArrayList<State> stateList= object.getStateList();
     		if (link.getLinkType() == LinkType.RESULT && link.getLabel() == "")
     		{
         		for(State currState : stateList)
         		{
         			if(link.getDstId() == currState.getId())
         			{
         				caseExist[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
             					"ev_create"+"_"+processName+"_"+currPlace+"_"+objName+"_"+currPlaceObj+
             					"_"+currState.getName()+" = TRUE",
             					"!("+objName+"_"+currPlaceObj+"=notExist)",otherAsoocs),nextValue);
         				break;
         			}
         		}

         		if(caseExist[0] == "") //the object is without states or has an initial state
         		{
             		caseExist[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
             					"ev_create"+"_"+processName+"_"+currPlace+"_"+objName+"_"+currPlaceObj+" = TRUE",
             					"!("+objName+"_"+currPlaceObj+"=notExist)",otherAsoocs),nextValue);
         		}
     		}
     		//creating the assoc for modify links
     		else
     		{
     			caseExist[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
     					"ev_activate"+"_"+processName+"_"+currPlace+"= TRUE",
     					"!("+objName+"_"+currPlaceObj+"=notExist)",otherAsoocs),nextValue);
     		}


     		return caseExist;
     	}
		
		/**
		 * This function create the rule for the destroy assoc_proc_obj
		 * @param objName
		 * @param processFather
		 * @param childrenList
		 * @param currPlace
		 * @param currPlaceObj
		 * @param k
		 * @return
		 * @throws RulesUtilsException - when null parameters were sent to SmvOp
		 */
     	private String[] DestroyAssocProcToObj(SmvObject obj, SmvProcess processFather,  ArrayList<SmvProcess> childrenList, int currPlace, int currPlaceObj, int k) throws RulesUtilsException 
     	{
     		String nextValue = "FALSE";
     		
     		String[] caseExist = new String[3];   	
     		caseExist[0] = "";
     		caseExist[1] = "";
     		caseExist[2] = "";
     		
     		String objObjRules = "";
     		int i = 0;
     		
     		for (Assoc currAssoc : RulesUtils.assocObjObj)
     		{
     			if(currAssoc.getProcess().getId() == processFather.getId())
     			{
     				if( objObjRules == "" )
     				{
     					objObjRules = "( "+ currAssoc.getAssocString() + " = TRUE";
     				}
     				else if(i%4 == 0)
     				{
     					objObjRules = objObjRules + ") & ( " + currAssoc.getAssocString() + " = TRUE";
     				}
     				else
     				{
     					objObjRules = objObjRules + " | " + currAssoc.getAssocString() + " = TRUE";
     				}
     			}
     			i++;
     		}
     		
     		if(RulesUtils.assocObjObj.size() != 0)
     		{
     			objObjRules += " )";
     			
     			caseExist[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
     					"ev_terminate"+"_"+processFather.getName()+"_"+currPlace +" = 0", objObjRules)
     					,nextValue);
     			caseExist[1] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
     					"ev_halt"+"_"+processFather.getName()+"_"+currPlace +" = TRUE", objObjRules)
     					,nextValue);
     		}
     		else
     		{
     			caseExist[0] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
     					"ev_terminate"+"_"+processFather.getName()+"_"+currPlace +" = 0")
     					,nextValue);
     			caseExist[1] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
     					"ev_halt"+"_"+processFather.getName()+"_"+currPlace +" = TRUE")
     					,nextValue);
     		}
     		
     		//in case of ev_consumption_object_i_childProcess_j : destroy assoc_fatherProcess_object     		
     		for(SmvProcess currChild: childrenList)
     		{
     			for(Link currLink : currChild.getLinkList())
     			{
     				if(currLink.getLinkType() == LinkType.CONSUMPTION && currLink.getLabel() == "")
     				{
     					if(currLink.getSrcType() == SmvType.STATE)
     					{
     						State relatedState = db.getSmvStateList().get(db.findStateById(currLink.getSrcId()));
     						
     						if((obj.getId() == relatedState.getObjectId()) && (currLink.getSrcId() == relatedState.getId()))
     						{
     							caseExist[2] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
     								"ev_consumption"+"_"+obj.getName()+"_"+currPlaceObj+"_"+relatedState.getName()+"_"+currChild.getName()+"_"+currPlace+" = TRUE")
     								,nextValue);
     						}
     					}
     					else // currLink.getSrcType() == SmvType.OBJECT
     					{
     						if( currLink.getSrcId() == obj.getId())
     						{
     							caseExist[2] = SmvOp.createCaseLine(SmvOp.and("sysState = step2 ",
     								"ev_consumption"+"_"+obj.getName()+"_"+currPlaceObj+"_"+currChild.getName()+"_"+currPlace+" = TRUE")
     								,nextValue);
     						}
     					}
     				}
     			}	
     		}
     		
     		
			return caseExist;
		}

     	/**
     	 * This function create the rule for assoc_obj_obj
     	 * @param fatherProcess
     	 * @return rule for assoc_obj_obj
     	 * @throws RulesUtilsException - when null parameters were sent to SmvOp
     	 */
    	private String createRuleForAssocObjects(SmvProcess fatherProcess) throws RulesUtilsException
         {
            
            String rules = "";
            String srcRes = "";
            String dstRes = "";
             
            for(Assoc currObjObj : RulesUtils.assocObjObj)
            {
                String rullForCreate = "";
                String rullForDestroy = "";           
                
                for(int i=0;i<SMVCreator.K;i++)
                {                
                	//build rule for create assoc_obj_obj
                	
            		srcRes = RulesUtils.findAssoc(currObjObj.getSrcName(), fatherProcess.getName()+"_"+i);
                    dstRes = RulesUtils.findAssoc(currObjObj.getDstName(), fatherProcess.getName()+"_"+i);
                    
                    if(srcRes!="" && dstRes!="")
                    {
                        if(rullForCreate != "")
                        {
                        	rullForCreate =  SmvOp.or(rullForCreate, SmvOp.and(srcRes + " = TRUE", dstRes + " = TRUE"));
                        }
                        else
                        {
                        	rullForCreate += SmvOp.and(srcRes + " = TRUE", dstRes + " = TRUE");
                        }
                    }
                }
                
                //build rule for destroy assoc_obj_obj - if ev_consumption_obj_childProc is TRUE destroy all objects that related to obj
                for(SmvProcess currChild : db.getChildrenList(fatherProcess))
         		{
         			for(Link currLink : currChild.getLinkList())
         			{
         				if(currLink.getLinkType() == LinkType.CONSUMPTION)
         				{
         					//src of consumption link is state
         					if(currLink.getSrcType() == SmvType.STATE)
             				{
             					//in case of src object in assoc relation has state
             					if(currObjObj.getSrcState() != null)
             					{
             						if(currLink.getSrcId() == currObjObj.getSrcState().getId())
                     				{
                     					 for(int i=0;i<SMVCreator.K;i++)
                     					 {
                     						if(rullForDestroy == "") rullForDestroy = "ev_consumption"+"_"+currObjObj.getSrcName()+"_"+currObjObj.getSrcState().getName()+"_"+currChild.getName()+"_"+i+" = TRUE";
                     						else rullForDestroy = SmvOp.or(rullForDestroy, "ev_consumption"+"_"+currObjObj.getSrcName()+"_"+currObjObj.getSrcState().getName()+"_"+currChild.getName()+"_"+i+" = TRUE");
                     					 } 			
                     					 rullForDestroy = SmvOp.and(rullForDestroy, "sysState = step2 ");		         					
                     				}
             					}
             					//in case of dst object in assoc relation has state
             					else if(currObjObj.getDstState() != null)
             					{
             						if (currLink.getSrcId() == currObjObj.getDstState().getId())
                     				{      					
                     					for(int i=0;i<SMVCreator.K;i++)
                    					 {
                    						if(rullForDestroy == "") rullForDestroy = "ev_consumption"+"_"+currObjObj.getDstName()+"_"+currObjObj.getDstState().getName()+"_"+currChild.getName()+"_"+i+" = TRUE";
                    						else rullForDestroy = SmvOp.or(rullForDestroy, "ev_consumption"+"_"+currObjObj.getDstName()+"_"+currObjObj.getDstState().getName()+"_"+currChild.getName()+"_"+i+" = TRUE");
                    					 }
                     				}
             					}
         					}
         					
         					else //src of consumption link is object
         					{
         						//the object is the dst object in assoc relation
         						if(currLink.getSrcId() == currObjObj.getDstId()) 
         						{
         							 for(int i=0;i<SMVCreator.K;i++)
         							 {
         								if(rullForDestroy == "") rullForDestroy = "ev_consumption"+"_"+currObjObj.getDstName()+"_"+currChild.getName()+"_"+i+" = TRUE";
         								else rullForDestroy = SmvOp.or(rullForDestroy, "ev_consumption"+"_"+currObjObj.getDstName()+"_"+currChild.getName()+"_"+i+" = TRUE");
         							 } 			
         							 rullForDestroy = SmvOp.and(rullForDestroy, "sysState = step2 ");		         					
         						}
         						//the object is the dst object in assoc relation
         						else if(currLink.getSrcId() == currObjObj.getSrcId())
         						{
         							 for(int i=0;i<SMVCreator.K;i++)
         							 {
         								if(rullForDestroy == "") rullForDestroy = "ev_consumption"+"_"+currObjObj.getSrcName()+"_"+currChild.getName()+"_"+i+" = TRUE";
         								else rullForDestroy = SmvOp.or(rullForDestroy, "ev_consumption"+"_"+currObjObj.getSrcName()+"_"+currChild.getName()+"_"+i+" = TRUE");
         							 }
         							
         							 rullForDestroy = SmvOp.and(rullForDestroy, "sysState = step2 ");			
         						}
         					}			
         				}
         			}	
         		}
                if(rullForCreate != "" || rullForDestroy != "")
                {
	                rullForCreate = SmvOp.and(rullForCreate,"sysState = step2");
	                String procRule = "";
	                String[] casesLines = new String[3];
	                
	                if(rullForCreate != "") casesLines[0] = SmvOp.createCaseLine(rullForCreate, "TRUE"); // 1 => assoc_obj1_obj2 = 1
	                
	                if (rullForDestroy != "") casesLines[1] = SmvOp.createCaseLine(rullForDestroy, "FALSE");
	                else casesLines[1] = "";
	                
	                casesLines[2] = SmvOp.createCaseLine("TRUE" , currObjObj.getAssocString());
	                procRule = SmvOp.createCase(casesLines);
	                //preventing dups
         			if(currObjObj.getAssocString() != null && currObjObj.getAssocString() != "" && assocDict.get(currObjObj.getAssocString()) == null){
         				assocDict.put(currObjObj.getAssocString(), "");
         				procRule = SmvOp.next(currObjObj.getAssocString(), procRule);
         				rules += "\n" + procRule;
         			}
	               
                }
            }
                    
            return rules;
         }  
            	
     	/**
     	 * This function create assoc_proc_obj for xor/or
     	 * @param objName
     	 * @param processName
     	 * @param currXorList
     	 * @param orXor
     	 * @param currPlace
     	 * @param currPlaceObj
     	 * @param k
     	 * @param processFatherName 
     	 * @return 
     	 * @throws RulesUtilsException - when null parameters were sent to SmvOp
     	 */
		private ArrayList<String> CreateAssocXorObject(String objName, String processName,
     			ArrayList<Link> currXorList, boolean orXor,
     			int currPlace,int currPlaceObj, int k, String processFatherName) throws RulesUtilsException
		{
     		ArrayList<String> objs = null;
     		Enumeration<String> keys = null;
     		Dictionary<String, String> evXors = null;
     		
     		String currObjName = objName + "_" +currPlaceObj;
     		String nextValue = "TRUE";

     		try
     		{
     			objs = RulesUtils.getDstNames(currXorList,db);
     		} 
     		catch (SmvDBException e) 
     		{
     			e.printStackTrace();
     		}
     		try 
     		{
     			evXors = RulesUtils.getXorDict(processName, objs, orXor);
     			keys = evXors.keys();		
     		} 
     		catch (RulesUtilsException e) 
     		{
     			e.printStackTrace();
     		}
     		
     		ArrayList<String> caseExist = new ArrayList<String>();
     		int i =0;
     		String otherAsoocs = "";
     		for (int j =0 ;j < SMVCreator.K;j++)
     		{
     			if (j != currPlaceObj)
     			{
     				otherAsoocs = SmvOp.and(otherAsoocs, "assoc"+"_"+processFatherName+
     									"_"+currPlace+"_"+objName+"_"+j+"=FALSE");
     			}
     		}
     		while (keys.hasMoreElements()) 
     		{	
     			String currEventName = keys.nextElement();
     			if (currEventName.contains(currObjName) && currEventName.contains(processName + "_" + currPlace))
     			{
 					//OR
     				if (false == orXor )
     					{
     						String[] elem = evXors.get(currEventName).split(",");
     						
     						//creating this type of lines:
     						//sysState = step2  & ev_or_proc1_son1_0_father1_1_father2_1_father3_0=father3_0_
     						for (String elm : elem)
     						{
     							if (elm.contains(currObjName))
     							{
     								caseExist.add(i, SmvOp.createCaseLine
     								(SmvOp.and("sysState = step2 ",
     								currEventName+"="+elm,"!("+currObjName+"=notExist)" ,otherAsoocs),nextValue));
     								i++;
     							}
     						}
     					}

     					else
     					{
     						caseExist.add(i, SmvOp.createCaseLine(SmvOp.and
     								("sysState = step2 ",
     								currEventName+"="+currObjName+"_","!("+currObjName+"=notExist)",otherAsoocs),
     								nextValue));
     						i++;
     					}
     			
     				}
     			}
     		return caseExist;
     	}
    	
    	private String[] toArray(ArrayList<String> createAssocXorObject) 
 		{
 			String[] strArray = new String[createAssocXorObject.size()];
 			int i=0;
 			for(String str : createAssocXorObject)
 			{
 				strArray[i] = str;
 				i++;
 			}
 			return strArray;
 		}
 		
}
